-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(ring_theory/jacobson): Generalize proofs about Jacobson rings and polynomials #5520
Conversation
…polynomial ring proofs
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
First comments. I haven't looked at the longer proofs yet.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The code looks good!
I'm wondering how easy it would be to "generalize" your results from "for all maximal ideals, the quotient map ..." to "for all ring homs that are surjective onto a field, ...". (Even though they should be equivalent, the latter contains more free variables in its conclusion: it might be easier to use in practice.) Have you considered the surjective map case already?
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
I think this is possible to do, but the trouble I had is that the proof needs to derive that certain other rings are actually fields by pulling across the homomorphisms, and the interface for |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm hqppy with merging this as it currently stands, and deriving the "surjective to a field" conclusion later, since it needs more work in other parts.
@jcommelin, what do you think?
@Vierkantor I realized there are much simpler proofs to the field surjection versions of the lemmas than the proofs I was picturing. I've just added them to this PR since they don't actually require many other changes elsewhere. |
Fantastic 😄 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fantastic! Thanks for adding the variants for surjecive maps. 🎉
bors merge
…d polynomials (#5520) These changes are meant to make deriving the classical nullstellensatz from the generalized version about Jacobson rings much easier and much more direct. `is_integral_localization_map_polynomial_quotient` already exists in the proof of a previous theorem, and this just pulls it out into an independent lemma. `polynomial.quotient_mk_comp_C_is_integral_of_jacobson` and `mv_polynomial.quotient_mk_comp_C_is_integral_of_jacobson` are the two main new statements, most of the rest of the changes are just generalizations and reorganizations of the existing theorems. Co-authored-by: Devon Tuma <dtumad@gmail.com>
Build failed (retrying...): |
…d polynomials (#5520) These changes are meant to make deriving the classical nullstellensatz from the generalized version about Jacobson rings much easier and much more direct. `is_integral_localization_map_polynomial_quotient` already exists in the proof of a previous theorem, and this just pulls it out into an independent lemma. `polynomial.quotient_mk_comp_C_is_integral_of_jacobson` and `mv_polynomial.quotient_mk_comp_C_is_integral_of_jacobson` are the two main new statements, most of the rest of the changes are just generalizations and reorganizations of the existing theorems. Co-authored-by: Devon Tuma <dtumad@gmail.com>
Build failed (retrying...): |
…d polynomials (#5520) These changes are meant to make deriving the classical nullstellensatz from the generalized version about Jacobson rings much easier and much more direct. `is_integral_localization_map_polynomial_quotient` already exists in the proof of a previous theorem, and this just pulls it out into an independent lemma. `polynomial.quotient_mk_comp_C_is_integral_of_jacobson` and `mv_polynomial.quotient_mk_comp_C_is_integral_of_jacobson` are the two main new statements, most of the rest of the changes are just generalizations and reorganizations of the existing theorems. Co-authored-by: Devon Tuma <dtumad@gmail.com>
Pull request successfully merged into master. Build succeeded: |
These changes are meant to make deriving the classical nullstellensatz from the generalized version about Jacobson rings much easier and much more direct.
is_integral_localization_map_polynomial_quotient
already exists in the proof of a previous theorem, and this just pulls it out into an independent lemma.polynomial.quotient_mk_comp_C_is_integral_of_jacobson
andmv_polynomial.quotient_mk_comp_C_is_integral_of_jacobson
are the two main new statements, most of the rest of the changes are just generalizations and reorganizations of the existing theorems.